package agent.ccs
import cwb.CWBParseException
import cwb.Value
import agent.Action
import agent.AgTau
import agent.Action


abstract class CCSAction extends Ordered[CCSAction] with Action { // Ordered[Action] {
  // True for In, false for Out
  def polarity: Boolean  = false // False per default
  
  def le(rhs: CCSAction): Boolean
    
  def equals(rhs: Any): Boolean
  

  val observable: Boolean
  
  /**
   * mkstr() returns the string representation of the action.
   * @return string representation of the action
   */
  def mkstr(): String
  

  def ge(rhs: CCSAction) = this >= rhs
  
  def geAction(act: Action) = {
    act.asInstanceOf[CCSAction] >= this
  }
  def leAction(act: Action) = {
    act.asInstanceOf[CCSAction] <= this
  }
  
  def valueOf: Option[Value] = None
  
  def isInput: Option[Boolean] = None
  
}

// Pol is true for in and false for out.
case class Act(port: Symbol, pol: Boolean, value: Option[Value]) extends CCSAction {
  override
  val observable = true
  
  override
  def polarity = pol
  
  override
  def compare(rhs: CCSAction) = {
    if (rhs.getClass == classOf[Act]) {
      val rha = rhs.asInstanceOf[Act]
      if (pol && !rha.pol) -1
      else if (!pol && rha.pol) 1
      else if (port == rha.port) {
        actValLe(rhs.asInstanceOf[Act])
      } else if (port.name < rha.port.name) -1
      else 1
    }
    else 1
  }
  

  
  def actValLe(rhs: Act): Int = {
    (value, rhs.value) match {
      case (None, None) => 0
      case (None, _) => -1
      case (_, None) => 1
      case (Some(a), Some(b)) => a.compareTo(b)
    }
  }
  
  // Returns the pole opposite of the act (a -> 'a)
  def inverse(): Act = new Act (port, !pol, value)
  
  // Equal if same underlying structure and polarity
  override
  def equals(rhs: Any) = {
    rhs match {
      case a: Act => {
       val act = a.asInstanceOf[Act]
       act.port == port && act.polarity == polarity && act.value == value
      }
      case _ => false
    }
  }

  def le(rhs: CCSAction) = rhs <= this
                                            
  override
  def hashCode() = port.hashCode()
  
  override
  def mkstr() = if (pol) port.name else "'" + port.name
  
  override
  def valueOf = value
  
  override
  // Returns Some(True) if input and Some(False) otherwise.
  def isInput = Some(polarity)
  
  def isInverseOf(other: Act): Boolean = port == other.port && pol != other.pol
  
  
  // Returns a copy of the current act with a modification according to other.
  def change(other: Act): Act = {
    new Act(other.port, if (pol) other.pol else !other.pol, value)
  }
  
  
  
  // TODO(gustafa): Makes sense? a -> a -> tau = tau?
}


case class Step() extends CCSAction {
  override
  // Step > Eps, Step > Tau
  def le(rhs: CCSAction) = rhs.getClass() != classOf[Tau] || rhs.getClass != classOf[Eps]
  
  override
  def equals(rhs: Any) = rhs.getClass() == classOf[Step]
  
  override
  def compare(rhs: CCSAction): Int = {
    rhs match {
      case _: Step => 0
      case _: Eps => 1
      case _: Tau => 1
      case _ => -1
    }
  }
  
  def mkstr() = "Step"
  
  override
  val observable = true
  
  override
  def hashCode() = 11
}


case class Tau(a: Option[CCSAction]) extends CCSAction with AgTau {
  val tau_of = a
  // Mark Tau as a non observable action
  
  // Only equal when both are Tau
  override
  def equals(rhs: Any): Boolean = rhs.getClass() == classOf[Tau]
  

  def mkstr() = "tau"
    
  def compare(rhs: CCSAction) = {
    rhs match {
      case _: Tau => 0
      case _ => -1
    }
  }
  
  
  override
  def le(rhs: CCSAction): Boolean = true

  override
  val observable: Boolean = false

  override
  def hashCode() = 5
}


case class Eps extends CCSAction {
  // Mark Eps as a non observable action
  override
  val observable: Boolean = false
  
    // Only equal when both are Eps
  override
  def equals(rhs: Any): Boolean = rhs.getClass() == classOf[Eps]
  
 def compare(rhs: CCSAction) = {
    rhs match {
      case _: Eps => 0
      case _: Tau => 1
      case _ => -1
    }
  }
  
  def mkstr() = "Eps"
  
  // Eps > Tau
  override
  def le(rhs: CCSAction) = rhs.getClass() != classOf[Tau]
  
  override
  def hashCode() = 7
  
}

object CCSAction {
  /**
   * makeAction takes a string and an optional parameter (TODO: drop this?), creates
   * an appropriate action from the string and returns this.
   * @param id string to be converted into an action.
   * @value parameter.
   * @return a ccs action corresponding to the given string.
   */
  def makeAction(id: String, value: Option[Value]): CCSAction = {
    val (polarity, name) = grab(id)
    name match {
      case "tau" => Tau(None)
      case "eps" => Eps()
      case "1" => Step()
      case _ => Act(Symbol(name), polarity, value)
    }    
    
  }
  
  /**
   * Creates an action from the given string.
   * @param s string to make an action from.
   * @return the action as represented by the string.
   */
  def mkact(s: String) = makeAction(s, None)
  
  /**
   * Grab takes a string such as 'a and returns (true, "a") for in and (false, "a") for out.
   */
  def grab(str: String): (Boolean, String) =  {
    if (str.length == 0) {
      throw new CWBParseException("Given 0 length action")
    }
    str.charAt(0) match {
      // Strip the polarity char
      case '\'' => (false, str.takeRight(str.length - 1))
      case _ => (true, str)
    }
  }
  
  /**
   * inverses checks whether the two actions are inverses of each other e.g. a and a'
   * An inverse implies input => output and output => input for acts.
   * Creates a Tau action for the two if so and returns whether the first parameter
   * is the sender. If not inverses simply returns None.
   * @param left action to check for inversion
   * @param right action to check for inversion
   * @return Option(left == sender, tau, constraints)  
   */
  def inverses(left: CCSAction, right: CCSAction): Option[(Boolean, Tau, Any)] = {
    (left, right) match {
      case (x: Act, y: Act) =>
        if (x.isInverseOf(y)) {
          val (sender, receiver) = if (x.pol) (y,x) else (x,y)
          val valueMaybe = sender.value
          val resultant = Tau (Some(Act(x.port, true, valueMaybe)))
          val extraConstraint = receiver.value match {
            case None => None
            case Some(valueR) => valueMaybe match {
            case None => System.out.println("FOO ERROR Inverses")
          //case   // TODO add makeEqualConstraint. TODO(gustafa): ADD MORE CONSTRAINTS
            }
          }
          Some(x == sender, resultant, extraConstraint)
        } else {
          None
        }
      case (_, _) => None
    }
  }
}